perm filename CODE.DOC[BMP,SYS] blob
sn#744791 filedate 1984-03-09 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00007 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002
C00006 00003 2
C00010 00004 3
C00013 00005 4
C00016 00006 5
C00018 00007 6
C00019 ENDMK
C⊗;
A POOR SUBSTITUTE FOR
A USER'S MANUAL FOR
A THEOREM PROVER FOR
A COMPUTATIONAL LOGIC
Robert S. Boyer and J Strother Moore
November 1983
CAVEAT
We are currently converting our theorem-proving system from Interlisp-10 to
the Maclisp family of languages. The conversion is not yet complete and will
not be complete until we have carefully scrutinized the new version. For a
variety of reasons, including speed and soundness, we have decided to stop
sending out the Interlisp version. We are sending out the current Maclisp
version with a major caveat: we do not yet vouch for the soundness of this
system. We know of no bugs. Write later for a vouched-for version.
THE THEORY
The mathematical theory in which our system proves theorems is described by
(a) Chapter III of A Computational Logic (1) (b) pages 133-136 of The
Correctness Problem in Computer Science (2), and (c) the rules about QUOTE
hinted at below. Note that we now use hyphen instead of period in identifiers
-- e.g., LEGAL-CHAR-CODE-SEQ instead of the former LEGAL.CHAR.CODE.SEQ.
DIRECTORIES
The theorem-prover currently resides on two directories at UTEXAS-20.ARPA:
AUX:<CL.THM> and AUX:<CL.PROOFS>. These two directories are provided as
distinct save sets when we send out our system on tape. Below, we sometimes
prefix file names with one of these two directories. At another site, you'll
have to find out from whoever installed the system which directory names to
use.
RUNNING THE THEOREM-PROVER
To start the theorem-prover, run the file AUX:<CL.THM>THM.EXE. THM is a
saved version of a Maclisp loaded with the theorem-prover's compiled files.
All of the theorem-prover commands are LISP programs. Next, initialize the
theorem-prover in one of two ways:
1. Call (BOOT-STRAP), putting the theorem-prover into its most
elementary state, or
2. Call (NOTE-LIB "foo.LIB" "foo.LISP"), putting the theorem-prover
into the state that it had when the command (MAKE.LIB "foo") was
invoked, which created the files "foo.LIB" and "foo.LISP". For
example, one might say
2
(NOTE-LIB "AUX:<CL.PROOFS>BOOT-STRAP.LIB"
"AUX:<CL.PROOFS>BOOT-STRAP.LISP") or
(NOTE-LIB "AUX:<CL.PROOFS>PROVEALL.LIB"
"AUX:<CL.PROOFS>PROVEALL.LISP").
An examination of the file AUX:<CL.PROOFS>XXXS.LISP will reveal hundreds of
examples of invocations of theorem-prover commands. Here we briefly list some
commonly used commands.
Command: (DEFN name args body hints)
Example: (DEFN APPEND (X Y)
(IF (LISTP X)
(CONS (CAR X) (APPEND (CDR X) Y))
Y))
This command attempts to admit name as a function under our principle of
definition. The optional fourth argument, hints, may be used to specify the
measure and well-founded relation. For examples look at the definitions of GCD
and NORMALIZE in the file XXXS.LISP.
Command: (PROVE-LEMMA name types term hints)
Example: (PROVE-LEMMA ASSOC-OF-APPEND (REWRITE)
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X (APPEND Y Z))))
This command attempts to prove term and to store it as a lemma of the types
specified. types may be any subset of (REWRITE ELIM GENERALIZE META). The
optional fourth argument, hints, may be used to specify instantiations of
previously proved lemmas to be used, the names of lemmas that are not to be
used, and the first induction to be done. See the PROVE-LEMMA commands for
TIMES-MOD-2 and PIGEON-HOLE-PRINCIPLE in the file XXXS.LISP.
Command: (TOGGLE name oldname flg)
Example: (TOGGLE ASSOC-APPEND-OFF ASSOC-OF-APPEND T)
If flg is T, TOGGLE prohibits future utilization of the theorem or definition
oldname. If flg is NIL, it turns oldname back on.
Command: (PROVEALL event-list NIL root)
Example: (PROVEALL '((DEFN BAR (X) (PLUS X X))
(PROVE-LEMMA BAR2 (REWRITE)
(EQUAL (BAR X) (TIMES 2 X))))
NIL
"BAR")
PROVEALL attempts to process the instructions on event-list. Output goes to
root.PROOFS and root.TTY (for errors and warnings). When finished, the files
root.LIB and root.LISP are created.
3
Command: (EVENTS-SINCE name)
Example: (EVENTS-SINCE 'APPEND)
This command returns the list of commands since the event named name.
Command: (UNDO-BACK-THROUGH name)
Example: (UNDO-BACK-THROUGH 'APPEND)
This command undoes all of the commands since the event named name.
QUOTE VS. "
In our two books we denote literal atoms with double quotation marks, e.g.
"PUSHV". When using the theorem-prover, one must use the notation (QUOTE
PUSHV) instead of "PUSHV". QUOTE may be given Sexpressions. The meaning of
(QUOTE (A B)) is the same as the meaning of (CONS (QUOTE A) (CONS (QUOTE B)
NIL)). Observe that the Maclisp reader reads 'PUSHV as (QUOTE PUSHV) and '(A
B) as (QUOTE (A B)).
BUILDING THE THEOREM PROVER IN MACLISP
The theorem-prover is created by running
PS:MACLISP AUX:<CL.THM>LISP.INI,
(MAKE-THM) ; A function defined in LISP.INI
SAVE THM.EXE 0 777
The theorem-prover is compiled (with the file AUX:<CL.THM>COMPLR.INI on the
directory of whoever is doing the compiling), by
<MACLISP>COMPLR.EXE
BASIS.LISP(W)
CROCK1.LSP ;Loads Basis
GENFACT.LISP(W)
CROCK2.LSP ;Loads Genfact
EVENTS.LISP(W)
CROCK3.LSP ;Loads Events
CODE-1-A.LISP(W)
CODE-B-D.LISP(W)
CODE-E-M.LISP(W)
CODE-N-R.LISP(W)
CODE-S-Z.LISP(W)
IO.LISP(W)
PPR.LISP(W).
4
RUNNING FUNCTIONS IN THE THEORY
It is possible to ask for the execution of variable free terms. For example,
if the logical function FLATTEN is defined in the usual way, then one may
execute
(R '(FLATTEN (QUOTE ((A B) (C D)))))
which will return
(A B NIL C D NIL NIL).
Because the Maclisp compiler is not resident within the theorem-prover due to
space limitations, the Maclisp functions that are generated by DEFN are EXPRs,
i.e., they are interpreted. To get the speed of compiled code, you may compile
a foo.LISP file produced by MAKE.LIB (assuming it is on the directory to which
you are currently connected) with following procedure:
1. Make sure that AUX:<CL.THM>COMPLR.INI has been copied to your
directory as COMPLR.INI.
2. Run PS:<MACLISP>COMPLR.
3. After receiving the ← prompt, type
CROCK1.UNFASL←AUX:<CL.THM>CROCK1.LSP{return}
4. Then type foo.LISP{return}
The file foo.FASL will have been created.
Then you may (NOTE-LIB "FOO.LIB" "FOO.FASL").
THE TAPE
The tape that we are currently sending out is written by a DEC-2060 running
TOPS-20 operating system version 5.3 at 1600 BPI with DUMPER. We have not yet
had any experience exporting this version of our theorem-prover, so it is
possible that we have failed to include sufficient files. However, we strongly
believe that we have included everything needed. The tape is made with the
DUMPER commands listed below.
The first "save set" contains the 370 page file THM.EXE, which is the
theorem-prover. No other file is essential for using the theorem-prover. Also
included in the first save set are all of the sources for the theorem-prover
and all of the compiler output.
5
On the second save set are several thousand pages of examples of input and
output. Files with the extension .PROOFS and .TTY are output intended for
human consumption. Files with the extension .LIB and .LISP are produced by
NOTE-LIB, as described above. The file XXXS.LISP contains the input that
produces all of the output.
The third save set contains the version of Maclisp used to build the system.
The fourth save set contains all of our ps:<maclisp> directory, and it is
only distributed on the off chance that someone will want to change and rebuild
our system.
dumper
interchange
rewind
save aux:<cl.thm>*.*.0
save aux:<cl.proofs>*.*.0
save ps:maclisp.exe.0
save ps:<maclisp>*.*.0
rewind
exit
6
REFERENCES
1. R. S. Boyer and J S. Moore. A Computational Logic. Academic Press, New
York, 1979.
2. R. S. Boyer and J S. Moore. Metafunctions: Proving Them Correct and Using
Them Efficiently as New Proof Procedures. In The Correctness Problem in
Computer Science, R. S. Boyer and J S. Moore, Eds., Academic Press, London,
1981.